Problem:
0(1(1(2(x1)))) -> 1(3(0(1(2(x1)))))
0(1(1(2(x1)))) -> 1(3(1(0(2(x1)))))
0(1(1(2(x1)))) -> 2(3(1(3(0(1(x1))))))
0(1(2(0(x1)))) -> 1(0(0(2(2(x1)))))
0(1(2(4(x1)))) -> 0(2(3(4(1(x1)))))
0(1(2(4(x1)))) -> 1(0(4(2(3(x1)))))
0(1(2(4(x1)))) -> 1(2(3(0(4(x1)))))
0(1(2(4(x1)))) -> 2(1(4(0(3(x1)))))
0(1(2(4(x1)))) -> 1(2(3(4(0(5(x1))))))
0(1(2(4(x1)))) -> 2(1(1(0(3(4(x1))))))
0(1(2(4(x1)))) -> 4(1(2(2(3(0(x1))))))
0(1(2(4(x1)))) -> 4(5(0(2(3(1(x1))))))
0(4(2(0(x1)))) -> 0(4(2(3(0(x1)))))
0(4(2(0(x1)))) -> 2(3(0(4(0(0(x1))))))
0(4(2(0(x1)))) -> 3(4(0(2(3(0(x1))))))
0(4(2(0(x1)))) -> 4(2(3(0(4(0(x1))))))
0(4(2(0(x1)))) -> 4(3(0(0(5(2(x1))))))
0(4(2(4(x1)))) -> 4(0(2(3(1(4(x1))))))
0(4(2(4(x1)))) -> 4(0(4(2(0(3(x1))))))
5(1(2(0(x1)))) -> 2(1(3(5(0(x1)))))
5(1(2(0(x1)))) -> 3(1(0(2(5(x1)))))
5(1(2(0(x1)))) -> 2(3(0(0(1(5(x1))))))
5(1(2(4(x1)))) -> 3(2(5(1(4(x1)))))
5(1(2(4(x1)))) -> 5(2(1(3(4(x1)))))
5(1(2(4(x1)))) -> 5(5(2(1(4(x1)))))
5(1(2(4(x1)))) -> 0(3(4(5(2(1(x1))))))
5(1(4(2(x1)))) -> 3(4(5(2(1(x1)))))
5(1(4(2(x1)))) -> 2(1(3(4(5(4(x1))))))
5(1(4(2(x1)))) -> 3(3(4(2(1(5(x1))))))
5(4(1(4(x1)))) -> 3(4(4(1(5(4(x1))))))
5(4(1(4(x1)))) -> 4(1(3(5(0(4(x1))))))
5(4(1(4(x1)))) -> 5(1(3(4(5(4(x1))))))
5(4(1(4(x1)))) -> 5(1(5(3(4(4(x1))))))
5(4(2(0(x1)))) -> 5(4(2(3(0(x1)))))
5(4(2(0(x1)))) -> 0(1(2(3(4(5(x1))))))
5(4(2(0(x1)))) -> 4(5(3(3(0(2(x1))))))
0(1(2(0(4(x1))))) -> 0(2(4(1(3(0(x1))))))
0(1(2(0(4(x1))))) -> 2(0(3(4(0(1(x1))))))
0(1(2(0(4(x1))))) -> 4(0(2(3(1(0(x1))))))
0(1(4(2(2(x1))))) -> 1(2(3(4(0(2(x1))))))
5(0(1(2(4(x1))))) -> 3(0(2(1(4(5(x1))))))
5(1(2(2(4(x1))))) -> 5(2(2(1(4(5(x1))))))
5(1(2(4(0(x1))))) -> 5(0(2(1(3(4(x1))))))
5(1(2(4(0(x1))))) -> 5(0(3(2(1(4(x1))))))
5(1(3(1(4(x1))))) -> 1(5(1(3(4(0(x1))))))
5(1(4(1(2(x1))))) -> 2(1(5(3(4(1(x1))))))
5(4(1(1(4(x1))))) -> 1(1(3(4(5(4(x1))))))
5(4(1(4(0(x1))))) -> 3(4(0(4(5(1(x1))))))
5(4(3(2(0(x1))))) -> 5(4(0(3(2(3(x1))))))
5(4(5(2(0(x1))))) -> 5(0(5(4(4(2(x1))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6,5}
transitions:
11(242) -> 243*
11(157) -> 158*
11(274) -> 275*
11(57) -> 58*
11(47) -> 48*
11(32) -> 33*
11(194) -> 195*
11(119) -> 120*
11(261) -> 262*
11(59) -> 60*
11(256) -> 257*
11(44) -> 45*
11(151) -> 152*
11(303) -> 304*
11(298) -> 299*
11(51) -> 52*
11(213) -> 214*
11(11) -> 12*
11(305) -> 306*
11(8) -> 9*
11(317) -> 318*
31(10) -> 11*
31(97) -> 98*
31(87) -> 88*
31(259) -> 260*
31(179) -> 180*
31(154) -> 155*
31(149) -> 150*
31(286) -> 287*
31(69) -> 70*
31(241) -> 242*
31(211) -> 212*
31(273) -> 274*
31(46) -> 47*
31(93) -> 94*
31(73) -> 74*
31(48) -> 49*
31(230) -> 231*
31(195) -> 196*
31(302) -> 303*
31(85) -> 86*
41(75) -> 76*
41(262) -> 263*
41(107) -> 108*
41(289) -> 290*
41(229) -> 230*
41(109) -> 110*
41(301) -> 302*
41(131) -> 132*
41(258) -> 259*
41(158) -> 159*
41(118) -> 119*
41(285) -> 286*
41(275) -> 276*
41(68) -> 69*
41(240) -> 241*
41(200) -> 201*
41(115) -> 116*
41(297) -> 298*
41(95) -> 96*
51(277) -> 278*
51(272) -> 273*
51(182) -> 183*
51(304) -> 305*
51(239) -> 240*
51(209) -> 210*
51(139) -> 140*
51(129) -> 130*
51(141) -> 142*
51(228) -> 229*
51(133) -> 134*
51(315) -> 316*
51(225) -> 226*
51(215) -> 216*
51(287) -> 288*
21(70) -> 71*
21(257) -> 258*
21(227) -> 228*
21(299) -> 300*
21(224) -> 225*
21(214) -> 215*
21(7) -> 8*
21(199) -> 200*
21(74) -> 75*
21(49) -> 50*
21(29) -> 30*
21(196) -> 197*
21(156) -> 157*
21(243) -> 244*
21(21) -> 22*
21(98) -> 99*
21(23) -> 24*
21(210) -> 211*
21(180) -> 181*
21(155) -> 156*
01(45) -> 46*
01(197) -> 198*
01(177) -> 178*
01(117) -> 118*
01(169) -> 170*
01(231) -> 232*
01(9) -> 10*
01(181) -> 182*
01(171) -> 172*
01(96) -> 97*
01(76) -> 77*
01(71) -> 72*
01(31) -> 32*
01(153) -> 154*
01(150) -> 151*
01(130) -> 131*
42(349) -> 350*
42(324) -> 325*
42(353) -> 354*
42(328) -> 329*
42(340) -> 341*
00(2) -> 5*
00(4) -> 5*
00(1) -> 5*
00(3) -> 5*
32(351) -> 352*
32(341) -> 342*
32(363) -> 364*
32(330) -> 331*
32(322) -> 323*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
02(339) -> 340*
02(329) -> 330*
02(361) -> 362*
02(321) -> 322*
02(350) -> 351*
02(325) -> 326*
02(362) -> 363*
02(327) -> 328*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
52(360) -> 361*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
22(359) -> 360*
22(331) -> 332*
22(323) -> 324*
22(352) -> 353*
40(2) -> 4*
40(4) -> 4*
40(1) -> 4*
40(3) -> 4*
50(2) -> 6*
50(4) -> 6*
50(1) -> 6*
50(3) -> 6*
1 -> 171,139,109,87,57,23
2 -> 153,129,95,73,44,7
3 -> 177,141,115,93,59,29
4 -> 169,133,107,85,51,21
8 -> 31*
12 -> 10,46,172,5
22 -> 8*
24 -> 8*
30 -> 8*
32 -> 289*
33 -> 10*
45 -> 227,179,68
50 -> 10,46,172,5
52 -> 45*
58 -> 45*
60 -> 45*
70 -> 315*
72 -> 46,172,301,10,5
74 -> 117*
77 -> 11*
86 -> 74*
88 -> 74*
94 -> 74*
96 -> 285,239,194,149
97 -> 272*
99 -> 11*
108 -> 96*
110 -> 96*
116 -> 96*
117 -> 359,321
118 -> 199*
120 -> 49*
130 -> 297,256
132 -> 97*
134 -> 130*
140 -> 130*
142 -> 130*
150 -> 213*
152 -> 119*
154 -> 301*
159 -> 170,97,46,172,301,10,5
170 -> 154*
172 -> 154*
178 -> 154*
183 -> 158*
195 -> 224,209
198 -> 158*
201 -> 197*
212 -> 210,140,130,297,6
216 -> 140,130,297,6
226 -> 215*
231 -> 240,134,261,210,140,6
232 -> 140,130,297,6
240 -> 261*
243 -> 317,277
244 -> 210,140,6
260 -> 211*
263 -> 229*
276 -> 240,134,130,297,261,6
278 -> 240,134,130,297,261,6
288 -> 242*
290 -> 97*
300 -> 214*
306 -> 140,130,297,6
316 -> 242*
318 -> 240,134,130,297,261,6
322 -> 349,327
324 -> 339*
326 -> 198,158
332 -> 198,158
342 -> 198,158
354 -> 198,158
364 -> 353*
problem:
Qed